 
import edu.mit.csail.sdg.alloy4.A4Reporter;
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.alloy4.ErrorWarning;
import edu.mit.csail.sdg.alloy4compiler.ast.Command;
import edu.mit.csail.sdg.alloy4compiler.ast.Module;
import edu.mit.csail.sdg.alloy4compiler.parser.CompUtil;
import edu.mit.csail.sdg.alloy4compiler.translator.A4Options;
import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution;
import edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod;
import edu.mit.csail.sdg.alloy4viz.VizGUI;

//Cette classe compile des fichiers
public class Compilateur {

    /*
     * Execute every command in every file.
     *
     * This method parses every file, then execute every command.
     *
     * If there are syntax or type errors, it may throw
     * a ErrorSyntax or ErrorType or ErrorAPI or ErrorFatal exception.
     * You should catch them and display them,
     * and they may contain filename/line/column information.
     */
    public static A4Solution trouverSolution(String[] args) throws Err {
        // The visualizer (We will initialize it to nonnull when we visualize an Alloy solution)
        VizGUI viz = null;
        // Alloy4 sends diagnostic messages and progress reports to the A4Reporter.
        // By default, the A4Reporter ignores all these events (but you can extend the A4Reporter to display the event for the user)
        A4Reporter rep = new A4Reporter() {
            // For example, here we choose to display each "warning" by printing it to System.out
            @Override public void warning(ErrorWarning msg) {
                System.out.print("Relevance Warning:\n"+(msg.toString().trim())+"\n\n");
                System.out.flush();
            }
        };

        for(String filename:args) {

            // Parse+typecheck the model
            System.out.println("=========== Parsing+Typechecking "+filename+" =============");
//System.out.println("SONDE");
            Module world = CompUtil.parseEverything_fromFile(rep, null, filename);
            // Choose some default options for how you want to execute the commands
            A4Options options = new A4Options();
            options.solver = A4Options.SatSolver.SAT4J;
            for (Command command: world.getAllCommands()) {
                // Execute the command
                System.out.println("============ Command "+command+": ============");
                A4Solution ans = TranslateAlloyToKodkod.execute_command(rep, world.getAllReachableSigs(), command, options);
                // Print the outcome
                //System.out.println(ans);
                // If satisfiable...
                if (ans.satisfiable()) {
                    // You can query "ans" to find out the values of each set or type.
                    // This can be useful for debugging.
                    //
                    // You can also write the outcome to an XML file
                    ans.writeXML(PlanbycoServer.CHEMINALS+PlanbycoServer.ALLOYRESULTAT);
                    //
                    // You can then visualize the XML file by calling this:

                    /*if (viz==null) {
                        viz = new VizGUI(false, "alloyResultat.xml", null);
                    } else {
                        viz.loadXML("alloyResultat.xml", true); 
			//ans.eval();
                    }*/

                }
                System.out.println("Fin complilation");
		return ans;
            }
        }
        return null;
    }
}
